from z3 import *

# 将整数映射到整数的数组A
A = Array("A", IntSort(), IntSort())
x, y = Ints("x y")

solve(A[x] == x, Store(A, x, y) == A)


a[i]  # select array 'a' at index 'i'
# Select(a, i)

Store(a, i, v)  # update array 'a' with value 'v' at index 'i'
# = Lambda(j, If(i == j, v, a[j]))

K(D, v)  # constant Array(D, R), where R is sort of 'v'.
# = Lambda(j, v)

Map(f, a)  # map function 'f' on values of 'a'
# = Lambda(j, f(a[j]))
Ext(a, b)  # Extensionality
# Implies(a[Ext(a, b)] == b[Ext(a, b)], a == b)

# For each occurrence in s of Store(a, i, v) and b[j], add the following assertions:
s.add(Store(a, i, v)[j] == If(i == j, v, a[j]))
s.add(Store(a, i, v)[i] == v)

#The theory of arrays is extensional. That is, two arrays are equal if they behave the same on all selected indices. When Z3 produces models for quantifier free formulas in the theory of extensional arrays it ensures that two arrays are equal in a model whenever they behave the same on all indices. Extensionality is enforced on array terms ,  in s by instantiating the axiom of extensionality.

s.add(Implies(ForAll(i, a[i] == b[i]), a == b))

# Since the universal quantifier occurs in a negative polarity we can introduce a Skolem function Ext that depends on a and b and represent the extensionality requirement as:
s.add(Implies(a[Ext(a, b)] == b[Ext(a, b)], a == b))